`timescale 1ns/1ns
module test (PR_if.TEST i1);


parameter aw = 5;
parameter dw = 32;

//***************************************************************************************** 
property p_rst_n;
@(negedge i1.cb.sys_clk)
(a1.rst_n          ==0)    |->  {(a1.PR_PC           =={aw{1'b0}} )&&
                                 (a1.Fet_Pkt_o       =={dw{1'b0}} )&&    
                                 (a1.PR_io_invalid   ==1 )&&
                                 (a1.FP_stall        ==a1.stall    )          };
endproperty                                             
a_rst_n:assert property (p_rst_n);                     



property p_DSP_core_en;
@(negedge i1.cb.sys_clk)
{(a1.rst_n          ==1)&&
 (a1.DSP_core_en    ==0)}  |->  {(a1.PR_PC           =={aw{1'b0}} )&&
                                 (a1.Fet_Pkt_o       =={dw{1'b0}} )&&    
                                 (a1.PR_io_invalid   ==1 )&&
                                 (a1.FP_stall        ==a1.stall )          };
endproperty                       
a_DSP_core_en:assert property (p_DSP_core_en);



property p_Int_Sev;
@(negedge i1.cb.sys_clk)
{(a1.rst_n          ==1)&&
 (a1.DSP_core_en    ==1)&&
 (a1.Int_Sev        ==1)}  |->  {(a1.PR_PC           =={aw{1'b0}} )&&
                                 (a1.Fet_Pkt_o       =={dw{1'b0}} )&&    
                                 (a1.PR_io_invalid   ==1 )&&
                                 (a1.FP_stall        ==a1.stall )          };
endproperty                       
a_Int_Sev:assert property (p_Int_Sev);




property p_PW_io_invalid;
@(negedge i1.cb.sys_clk)
{(a1.rst_n          ==1)&&
 (a1.DSP_core_en    ==1)&&
 (a1.Int_Sev        ==0)&&
 (a1.PW_io_invalid  ==1) }  |->       {(a1.PR_PC           ==$past(a1.PR_PC ,1))&&
                                       (a1.Fet_Pkt_o       ==$past(a1.Fet_Pkt_o ,1) )&&    
                                       (a1.PR_io_invalid   ==1 )&&
                                       (a1.FP_stall        ==a1.stall )          };
endproperty                       
a_PW_io_invalid:assert property (p_PW_io_invalid);



property p_PW_PC;
@(negedge i1.cb.sys_clk)
{(a1.rst_n          ==1)&&
 (a1.DSP_core_en    ==1)&&
 (a1.Int_Sev        ==0)&&
 (a1.PW_io_invalid  ==0)&&
 
 (a1.DP_stall       ==0)&&
 (a1.I_FP_invalid   ==0)&&
 (a1.D_RAM_invalid  ==0)}  |->  {(a1.PR_PC           ==a1.PW_PC )&&
                                 (a1.Fet_Pkt_o       ==a1.Fet_Pkt_i )&&    
                                 (a1.PR_io_invalid   ==0 )&&
                                 (a1.FP_stall        ==a1.stall )          };
endproperty                       
a_PW_PC:assert property (p_PW_PC);



property p_PR_PC;
@(negedge i1.cb.sys_clk)
{(a1.rst_n          ==1)&&
 (a1.DSP_core_en    ==1)&&
 (a1.Int_Sev        ==0)&&
 (a1.PW_io_invalid  ==0)&&
 !{(a1.DP_stall       ==0)&&
   (a1.I_FP_invalid   ==0)&&
   (a1.D_RAM_invalid  ==0)  } }  |->  {(a1.PR_PC           ==$past(a1.PR_PC ,1))&&
                                       (a1.Fet_Pkt_o       ==$past(a1.Fet_Pkt_o ,1) )&&    
                                       (a1.PR_io_invalid   ==0 )&&
                                       (a1.FP_stall        ==a1.stall )          };
endproperty                       
a_PR_PC:assert property (p_PR_PC);










//***************************************************************************************** 
class Randc_Range;
    rand bit  r0,r1,r2,r3,r4,r5,r6; 
    
    
    randc bit  [aw-1:0]rr0;
    randc bit  [dw-1:0]rr1;  
endclass

Randc_Range rr;

//*****************************************************************************************
initial 
 begin

repeat(3000)
@(posedge i1.cb.sys_clk)

  begin
     rr=new();
     assert (rr.randomize());

##1  i1.cb.rst_n=rr.r0;   
     i1.cb.DP_stall=rr.r1; 
     i1.cb.I_FP_invalid=rr.r2;
     i1.cb.D_RAM_invalid=rr.r3;
     i1.cb.PW_io_invalid=rr.r4;
     i1.cb.Int_Sev=rr.r5;
     i1.cb.DSP_core_en=rr.r6;
     i1.cb.PW_PC=rr.rr0;
     i1.cb.Fet_Pkt_i=rr.rr1;
   end
 end
//*****************************************************************************************  


endmodule